Nuprl Lemma : es-ble_wf 0,22

es:ES, ee':E. es-ble{i:l}(es;e;e'  
latex


DefinitionsP  Q, true, false, , es-ble{i:l}(es;e;e'), P  Q, decidable es-le, ES, E, Prop, Dec(P), e  e' , x:AB(x), t  T
Lemmases-le wf, decidable wf, es-E wf, event system wf, decidable es-le, bfalse wf, btrue wf

origin